$\forall$$A$:MsgA, $b$:Id, $s$, $s_{0}$:$A$.state.
\\[0ex]ma{-}frame{-}compat($A$;$A$)
\\[0ex]$\Rightarrow$ $b$ in dom($A$.pre)
\\[0ex]$\Rightarrow$ ($A$.pre($b$,$s$) $\Leftarrow\!\Rightarrow$ $A$.pre($b$,$\lambda$$x$.if $A$:locl($b$) may not read $x$ then $s_{0}$($x$) else $s$($x$) fi ))